`include "OperCarryBloc.sv"

// Multi-Operand Carry-Save Adder
// A parameterized adder that accepts 2^LEVEL operands.

module RecurCarrySaveAdder #(
  parameter WIDTH = 4,
  parameter LEVEL = 3,
  parameter OPERS = 1 << LEVEL
)
(
  input  logic [OPERS-1:0][WIDTH-1:0] Op,  // array of operands 
  output logic [WIDTH + LEVEL - 1:0] S,
  output logic cout
);

  logic [WIDTH-1:0] So;  // outgoing sum bits
  logic [WIDTH-2:0] Co;  // outgoing carry bits
  logic [LEVEL  :0] Coe; // outgiong extended carry bits (to next bloc, 1-bit gt than cie)

  assign {cout, S} = {Coe, So} + {{LEVEL{1'b0}}, Co, 1'b0};

  OperCarryBloc#(.WIDTH(WIDTH), .LEVEL(LEVEL))
  bloc (.Si(0), .Ci(0), .Cie(0), .*);

  `ifdef FORMAL
    wire logic [WIDTH+LEVEL+1:0] orig, calc;
    assign orig = Op[0] + Op[1] + Op[2] + Op[3] + Op[4] + Op[5] + Op[6] + Op[7];
    assign calc = {Coe, So} + {Co, 1'b0};

    always_comb begin
      (* anyconst *) logic[OPERS-1:0][WIDTH-1:0] anyOp;
      assume(Op == anyOp);
      A1: assert(orig == calc);
    end
  `endif

endmodule
